$\vdash$ $\mathbb{N}$ $\in$ Type